module sva_ca_implication_1;
    logic clk;
    initial begin
        clk = 0;
        forever #5 clk = ~clk;
    end

    logic a, b;
    initial begin
        a=1; b=1; #5;
        a=0; b=1; #10;
        a=1; b=1; #10;
        a=1; b=1; #10;
        a=0; b=0; #10;
        a=1; b=1; #10;
        $finish;
    end

    // 如果 a 在当前时钟上升沿为真, 则 b 在两个周期后的上升沿也必须为真.
    property p1;
        @(posedge clk) a |-> ##2 b;
    endproperty
    ap1: assert property(p1) $info("ap1 passed"); else $error("ap1 failed");

    // a 在当前时钟上升沿必须为真, 且 b 在两个时钟周期之后的上升沿也必须为真;
    // 若 a 在当前时钟边沿为假, 断言立即失败.
    property p2;
        @(posedge clk) a ##2 b;
    endproperty
    ap2: assert property(p2) $info("ap2 passed"); else $error("ap2 failed");

    initial begin
        $dumpfile("dump.vcd"); $dumpvars;
    end
endmodule

/* Output: QuestaSim
# ** Error: ap2 failed
#    Time: 15 ns Started: 15 ns  Scope: sva_ca_implication_1.ap2 File: sva_ca_implication_1.sv Line: 30
# ** Info: ap2 passed
#    Time: 25 ns Started: 5 ns  Scope: sva_ca_implication_1.ap2 File: sva_ca_implication_1.sv Line: 30
# ** Info: ap1 passed
#    Time: 25 ns Started: 5 ns  Scope: sva_ca_implication_1.ap1 File: sva_ca_implication_1.sv Line: 23
# ** Error: ap2 failed
#    Time: 45 ns Started: 45 ns  Scope: sva_ca_implication_1.ap2 File: sva_ca_implication_1.sv Line: 30
# ** Error: ap2 failed
#    Time: 45 ns Started: 25 ns  Scope: sva_ca_implication_1.ap2 File: sva_ca_implication_1.sv Line: 30
# ** Error: ap1 failed
#    Time: 45 ns Started: 25 ns  Scope: sva_ca_implication_1.ap1 File: sva_ca_implication_1.sv Line: 23
 */